COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	cancel[s88,jmc]		Propositional Cancellation logic
C00007 ENDMK
C⊗;
cancel[s88,jmc]		Propositional Cancellation logic

Propositional cancellation logic (pcl) has the primitive

(p kills q).

Its intended meaning is that if  p  is asserted and  (p kills q)  is
asserted then  q  is false even if it has been asserted.  Of course,
if we have  (p kills q)  and  (q kills p),  there will be trouble.
We may want to give such things an interpretation, but in the hoped-for
applications the set of formulas asserted will be suitably stratified.
We will be especially interested in sets of assertions with unique
interpretations.

Part of our goal is to use pcl to formalize some theory of events and
actions, e.g. some version of situation calculus.  There will be
obstacles, including unexpected obstacles, and events that overcome them.
We are hoping to keep the cancellation in the logic and avoid having
to include it in the event theory itself.

It seems we can allow complex formulas to be killed, e.g.

(p kills (q kills r))

is ok.

1. We need a definition of suitably stratified collection of formulas.

2. We need a notion of interpretation of a collection of formulas.
It runs as follows.

	a. It assigns truth or falsity to all formulas.

	b. Logical combinations obey the usual rules.

	c. Formulas in  A  are assigned TRUE unless cancelled and
are assigned FALSE if cancelled.

	d. If  p  is assigned TRUE and  (p kills q)  is assigned
TRUE, then  q  is cancelled.  However, consistency may require
that other formulas are cancelled, so we haven't fully defined
interpretation yet.  The example is

(1)	{p,(p kills r),q,q ⊃ r}.

If  r  is cancelled,  q  will have to be cancelled also.  It might
be desirable to require that all cancellation be explicit.  In that
case, (1) would not be a suitably stratified collection of
formulas.  However, I'd like to save it.

Examples:

1. {p,q,(p kills q)}

has the interpretation {(p T),(q F),((p kills q) T)}.

2. {(p kills p)}

is not suitably stratified.

3. {p,q,r,(p kills q),(r kills (p kills q))}

has the interpretation

 {(p T),(q T),(r T),((p kills q) F),((r kills (p kills q)) T)}.

4. {p,q,r,(p kills q),(r kills p)}

has the interpretation  {(p F),(q T),((p kills q) T),((r kills p) T)}.

5. {q,(p kills q)} may have more than one interpretation, since  p  is
not tied down.  On the other hand we may want to assume  p  false if
it is not mentioned.

Now I need examples with common sense content.

6.	∀x(bird x ⊃ flies x)

	∀x(ostrich x kills (bird x ⊃ flies x))

6.	a(x):(bird x ⊃ flies x)

	b(x):(ostrich x kills a(x))

bench[1,val]